es:ES, Cmd:Type, In:AbsInterface(Cmd), isupdate:(Cmd), Sys, Out:AbsInterface(Top).
(E(In) r E(Sys))
 (f:sys-antecedent(es;Sys), chain:(E(Sys)(Id List)).
 chain-consistent(f;chain)  (x, y:Id. x <<= y  y <<= x  (x = y))) 

latex

Up	abstract chain replication
Definitions	x <<= y, #$n, ||as||, P  Q, P  Q, a = b, loc(e), x before y  l, Atom$n, no_repeats(T;l), (x  l), adjacent(T;L;x;y), e loc e' , L1  L2, hd(l), a < b, x:A. B(x), {x:A| B(x)} , e c e', E, E(X), Top, P & Q, x. t(x), first(e), pred(e), A, x,y. t(x;y), pred!(e;e'), , SWellFounded(R(x;y)), constant_function(f;A;B), b, , e < e', r  s, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , type List, Msg(M), kind(e), loc(e), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), EOrderAxioms(E; pred?; info), IdLnk, Unit, EqDecider(T), , f(a), EState(T), P  Q, left + right, P  Q, strong-subtype(A;B), t  T, <a, b>, a:A fp B(a), x:A  B(x), x:A. B(x), x << y, s = t, chain-consistent(f;chain), sys-antecedent(es;Sys), x:AB(x), AbsInterface(A), Type, Id, ES, !Void(), False
Lemmas	chain-order-antireflexive, chain-order transitivity, Id wf, subtype rel wf, EState wf, rationals wf, member wf, strongwellfounded wf, pred! wf, loc wf, not wf, assert wf, constant function wf, kindcase wf, Knd wf, top wf, bool wf, cless wf, qle wf, val-axiom wf, nat wf, unit wf, Msg wf, IdLnk wf, EOrderAxioms wf, deq wf, es-E-interface wf, es-interface wf, es-E wf, es-causle wf, chain-order wf, assert-eq-id, rev implies wf, iff wf, or functionality wrt iff, chain-consistent wf, sys-antecedent wf, event system wf